FDL - Nuprl Lemma : R-state-var-init_wf

Nuprl Lemma : R-state-var-init_wf

i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, v:T, ks:(Knd List), tr:(k:{k:Knd|

i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, v:T, ks:(Knd List), tr:(k:{(k

ks)}

i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, v:T, ks:(Knd List), tr:(

decl-state

i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, v:T, ks:(Knd List), tr:(

(ds)

i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, v:T, ks:(Knd List), tr:(

ma-valtype

i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, v:T, ks:(Knd List), tr:(

(da; k)

i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, v:T, ks:(Knd List), tr:(

T

T).
fpf-compatible(Id; x.Type; id-deq; ds; fpf-single(x; T))

(R-state-var-init(i; ds; da; x; T; v; ks; tr)

es_realizer{i:l})

Definitions x. t(x), R-state-var-init(i; ds; da; x; T; v; ks; tr), t T, P Q, x:A. B(x), x(s), prop{i:l}

Lemmas fpf wf, ma-valtype wf, decl-state wf, l member wf, Knd wf, fpf-single wf3, id-deq wf, Id wf, fpf-compatible wf, rationals wf, Rinit wf, R-state-var wf, Rplus wf